
#include "ProblemData.h"

ProblemData::ProblemData(string filename)
{
	ifstream file;
	file.open (filename.c_str(), ifstream::in);
	
	if (file.is_open())
	{
		//First we get the parameters
		string s;
		
		file>>s;
		while(s == "c")
		{
			char c = 'a';
			while(c != '\n')
			{
				file.read(&c,1);
			}
			file>>s;
		}
		
		if(s != "p")
		{
			cerr << "Got "<<s<<", expected 'p'."<<endl;
			exit(EXIT_FAILURE);
		}
		
		file>>s;
		if(s != "cnf")
		{
			cerr << "Problem is not CNF"<<endl;
			exit(EXIT_FAILURE);
		}
		
		file >> nLiterals;
		nLiterals *= 2;
		
		file >> nClauses;
		
		literals.resize(nLiterals);
		
		//Now we read all clauses
		int n;
		
		for(int i=0; i < nClauses; i++)
		{
			set<int> clauses_literals;
			file >> n;
			
			while(n != 0)
			{
				if(n>0)
				{
					n -= 1;
				}
				else
				{
					//not literal (i) is literal (nLiterals-i-1)
					n += nLiterals;
				}
				
				literals[n].insert(i);
				clauses_literals.insert(n);
				
				file >> n;
			}

			clauses.insert(pair<int, set<int> >(i, clauses_literals));
		}
		
		file.close();
	}
	else
	{
		cerr << "Error opening "<<filename<<endl;
		exit(EXIT_FAILURE);
	}
}

void ProblemData::eraseClause(int c)
{
	const set<int> & clause_literals = clauses[c];

	for (set<int>::const_iterator it = clause_literals.begin(),
		 it_end = clause_literals.end(); it != it_end; ++it)
	{
		literals[*it].erase(c);
	}
	
	clauses.erase(c);
}

void ProblemData::print()
{
	cout<<nLiterals/2<<" variables, in "<<nClauses<<" clauses."<<endl<<endl;
	
	for(int i=0; i<nClauses; i++)
	{
		cout<<"Clause "<<i<<": (";

		set<int> clause_literals = clauses[i];
		if (clause_literals.size() > 0)
		{
			set<int>::iterator it = clause_literals.begin();
			set<int>::iterator it_end = clause_literals.end();

			if (*it < nLiterals/2)
			{
				cout<<"x"<<*it;
			}
			else
			{
				cout<<"not_x"<<(nLiterals-1-*it);
			}
			
			while (++it != it_end)
			{
				if (*it < nLiterals/2)
				{
					cout<<", x"<<*it;
				}
				else
				{
					cout<<", not_x"<<(nLiterals-1-*it);
				}
			}
		}
		
		cout<<")"<<endl;
	}
	/*cout<<endl;
	
	for(int i=0; i<nLiterals/2; i++)
	{
		cout<<"Literal x"<<i<<" in: (";
		
		if(literals[i].size() >= 1)
		{
			cout<<literals[i][0];
			
			for(unsigned int j=1; j<literals[i].size(); j++)
			{
				cout<<", "<<literals[i][j];
			}
		}
		
		cout<<")"<<endl;
		
		cout<<"Literal not_x"<<i<<" in: (";
		int not_i = nLiterals-1-i;
		
		if(literals[not_i].size() >= 1)
		{
			cout<<literals[not_i][0];
			
			for(unsigned int j=1; j<literals[not_i].size(); j++)
			{
				cout<<", "<<literals[not_i][j];
			}
		}
		
		cout<<")"<<endl;
	}*/
}

void ProblemData::checkSolution(Node sol)
{
	for(int i=0; i < nClauses; i++)
	{
		bool satisfied = false;
		int satVar=0;
		
		for (set<int>::const_iterator it = clauses[i].begin(),
			 it_end = clauses[i].end(); it != it_end; ++it)
		{
			satVar = *it;
			int var = satVar;
			
			if(var < nLiterals/2)
			{
				if(sol.varValues(var))
				{
					satisfied = true;
					break;
				}
			}
			else
			{
				var = nLiterals-1-var;
				if(!sol.varValues(var))
				{
					satisfied = true;
					break;
				}
			}
		}
		
		if(satisfied)
		{
			if(satVar < nLiterals/2)
			{
				cout<<"Clause "<<i<<" satisfied by x"<<satVar<<endl;
			}
			else
			{
				satVar = nLiterals-1-satVar;
				cout<<"Clause "<<i<<" satisfied by not_x"<<satVar<<endl;
			}
		}
		else
		{
			cout<<"/!\\ Clause "<<i<<" not satisfied!!!"<<endl;
		}
	}
}

